es:event_system{i:l}, e,e':es-E(es), l:IdLnk.
(e'  es-receives(es; e; l))
 ((es-isrcv(es; e')) c ((es-sender(es; e') = e)  (es-lnk(es; e') = l))) 

latex

Definitions

es-receives(es; e; l), (x  l), es-lnk(es; e), es-sender(es; e), x:A  B(x), es-isrcv(es; e), Type, prop{i:l}, A c B, P  Q, P  Q, f(a), Unit, left + right, first(e), A, idlnk-deq, es-eq(es), void, x:AB(x), False, rcv-from-on(dE; dL; info; e; l; r), {x:A| B(x)} , type List, subtype(S; T), receives(dE; dL; pred?; info; p; e; l), EOrderAxioms(E;pred?;info), event_system{i:l}, es_info(es), es-pred?(es), es-E(es), pred!(e;e'), SWellFounded(R(x;y)), es-oaxioms(es), t.1, destination(l), loc(e), Id, s = t, e < e', P  Q, P  Q, link(e), IdLnk, P  Q, sender(e), rcv?(e), b, x:A. B(x), x:A. B(x), t  T, loc(e), es-pred(es; e), es-first(es; e), kind(e), lnk(k), isrcv(k), es-kind(es; e)

Lemmas

isrcv wf, lnk wf, kind wf, rcv?-link, rcv?-kind, es-loc-pred, event system wf, es-oaxioms wf, EOrderAxioms wf, es-pred!-wellfounded, iff functionality wrt iff, member receives, receives wf, rcv-from-on wf, es-eq wf, idlnk-deq wf, not wf, first wf, unit wf, es-pred? wf, loc wf, rcv? wf, sender wf, link wf, Id wf, es info wf, assert wf, es-isrcv wf, es-sender wf, IdLnk wf, es-lnk wf, l member wf, es-E wf, es-receives wf